Nuprl Lemma : fpf_wf
11,40
postcript
pdf
A
:Type,
B
:(
A
Type). fpf(
A
;
a
.
B
(
a
))
Type
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
fpf(
A
;
a
.
B
(
a
))
,
x
(
s
)
,
prop{i:l}
Lemmas
l
member
wf
origin
A:Type, B:(A
Type). fpf(A; a.B(a)) 
Type A:Type, B:(AType). fpf(A; a.B(a)) Type x:A. B(x) T